Termination w.r.t. Q proof of TRS/nontermin/AG01#4.36.trs

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(m)) → false
eq(s(n), 0) → false
eq(s(n), s(m)) → eq(n, m)
le(0, m) → true
le(s(n), 0) → false
le(s(n), s(m)) → le(n, m)
min(cons(0, nil)) → 0
min(cons(s(n), nil)) → s(n)
min(cons(n, cons(m, x))) → if_min(le(n, m), cons(n, cons(m, x)))
if_min(true, cons(n, cons(m, x))) → min(cons(n, x))
if_min(false, cons(n, cons(m, x))) → min(cons(m, x))
replace(n, m, nil) → nil
replace(n, m, cons(k, x)) → if_replace(eq(n, k), n, m, cons(k, x))
if_replace(true, n, m, cons(k, x)) → cons(m, x)
if_replace(false, n, m, cons(k, x)) → cons(k, replace(n, m, x))
sort(nil) → nil
sort(cons(n, x)) → cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x)))

Q is empty.

↳ QTRS

  ↳ Overlay + Local Confluence

Q restricted rewrite system:
The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(m)) → false
eq(s(n), 0) → false
eq(s(n), s(m)) → eq(n, m)
le(0, m) → true
le(s(n), 0) → false
le(s(n), s(m)) → le(n, m)
min(cons(0, nil)) → 0
min(cons(s(n), nil)) → s(n)
min(cons(n, cons(m, x))) → if_min(le(n, m), cons(n, cons(m, x)))
if_min(true, cons(n, cons(m, x))) → min(cons(n, x))
if_min(false, cons(n, cons(m, x))) → min(cons(m, x))
replace(n, m, nil) → nil
replace(n, m, cons(k, x)) → if_replace(eq(n, k), n, m, cons(k, x))
if_replace(true, n, m, cons(k, x)) → cons(m, x)
if_replace(false, n, m, cons(k, x)) → cons(k, replace(n, m, x))
sort(nil) → nil
sort(cons(n, x)) → cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x)))

Q is empty.

The TRS is overlay and locally confluent. By [15] we can switch to innermost.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(m)) → false
eq(s(n), 0) → false
eq(s(n), s(m)) → eq(n, m)
le(0, m) → true
le(s(n), 0) → false
le(s(n), s(m)) → le(n, m)
min(cons(0, nil)) → 0
min(cons(s(n), nil)) → s(n)
min(cons(n, cons(m, x))) → if_min(le(n, m), cons(n, cons(m, x)))
if_min(true, cons(n, cons(m, x))) → min(cons(n, x))
if_min(false, cons(n, cons(m, x))) → min(cons(m, x))
replace(n, m, nil) → nil
replace(n, m, cons(k, x)) → if_replace(eq(n, k), n, m, cons(k, x))
if_replace(true, n, m, cons(k, x)) → cons(m, x)
if_replace(false, n, m, cons(k, x)) → cons(k, replace(n, m, x))
sort(nil) → nil
sort(cons(n, x)) → cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x)))

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(cons(0, nil))
min(cons(s(x0), nil))
min(cons(x0, cons(x1, x2)))
if_min(true, cons(x0, cons(x1, x2)))
if_min(false, cons(x0, cons(x1, x2)))
replace(x0, x1, nil)
replace(x0, x1, cons(x2, x3))
if_replace(true, x0, x1, cons(x2, x3))
if_replace(false, x0, x1, cons(x2, x3))
sort(nil)
sort(cons(x0, x1))

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

REPLACE(n, m, cons(k, x)) → IF_REPLACE(eq(n, k), n, m, cons(k, x))
EQ(s(n), s(m)) → EQ(n, m)
SORT(cons(n, x)) → REPLACE(min(cons(n, x)), n, x)
MIN(cons(n, cons(m, x))) → LE(n, m)
LE(s(n), s(m)) → LE(n, m)
SORT(cons(n, x)) → MIN(cons(n, x))
REPLACE(n, m, cons(k, x)) → EQ(n, k)
SORT(cons(n, x)) → SORT(replace(min(cons(n, x)), n, x))
IF_MIN(true, cons(n, cons(m, x))) → MIN(cons(n, x))
MIN(cons(n, cons(m, x))) → IF_MIN(le(n, m), cons(n, cons(m, x)))
IF_MIN(false, cons(n, cons(m, x))) → MIN(cons(m, x))
IF_REPLACE(false, n, m, cons(k, x)) → REPLACE(n, m, x)

The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(m)) → false
eq(s(n), 0) → false
eq(s(n), s(m)) → eq(n, m)
le(0, m) → true
le(s(n), 0) → false
le(s(n), s(m)) → le(n, m)
min(cons(0, nil)) → 0
min(cons(s(n), nil)) → s(n)
min(cons(n, cons(m, x))) → if_min(le(n, m), cons(n, cons(m, x)))
if_min(true, cons(n, cons(m, x))) → min(cons(n, x))
if_min(false, cons(n, cons(m, x))) → min(cons(m, x))
replace(n, m, nil) → nil
replace(n, m, cons(k, x)) → if_replace(eq(n, k), n, m, cons(k, x))
if_replace(true, n, m, cons(k, x)) → cons(m, x)
if_replace(false, n, m, cons(k, x)) → cons(k, replace(n, m, x))
sort(nil) → nil
sort(cons(n, x)) → cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x)))

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(cons(0, nil))
min(cons(s(x0), nil))
min(cons(x0, cons(x1, x2)))
if_min(true, cons(x0, cons(x1, x2)))
if_min(false, cons(x0, cons(x1, x2)))
replace(x0, x1, nil)
replace(x0, x1, cons(x2, x3))
if_replace(true, x0, x1, cons(x2, x3))
if_replace(false, x0, x1, cons(x2, x3))
sort(nil)
sort(cons(x0, x1))

We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

Q DP problem:
The TRS P consists of the following rules:

REPLACE(n, m, cons(k, x)) → IF_REPLACE(eq(n, k), n, m, cons(k, x))
EQ(s(n), s(m)) → EQ(n, m)
SORT(cons(n, x)) → REPLACE(min(cons(n, x)), n, x)
MIN(cons(n, cons(m, x))) → LE(n, m)
LE(s(n), s(m)) → LE(n, m)
SORT(cons(n, x)) → MIN(cons(n, x))
REPLACE(n, m, cons(k, x)) → EQ(n, k)
SORT(cons(n, x)) → SORT(replace(min(cons(n, x)), n, x))
IF_MIN(true, cons(n, cons(m, x))) → MIN(cons(n, x))
MIN(cons(n, cons(m, x))) → IF_MIN(le(n, m), cons(n, cons(m, x)))
IF_MIN(false, cons(n, cons(m, x))) → MIN(cons(m, x))
IF_REPLACE(false, n, m, cons(k, x)) → REPLACE(n, m, x)

The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(m)) → false
eq(s(n), 0) → false
eq(s(n), s(m)) → eq(n, m)
le(0, m) → true
le(s(n), 0) → false
le(s(n), s(m)) → le(n, m)
min(cons(0, nil)) → 0
min(cons(s(n), nil)) → s(n)
min(cons(n, cons(m, x))) → if_min(le(n, m), cons(n, cons(m, x)))
if_min(true, cons(n, cons(m, x))) → min(cons(n, x))
if_min(false, cons(n, cons(m, x))) → min(cons(m, x))
replace(n, m, nil) → nil
replace(n, m, cons(k, x)) → if_replace(eq(n, k), n, m, cons(k, x))
if_replace(true, n, m, cons(k, x)) → cons(m, x)
if_replace(false, n, m, cons(k, x)) → cons(k, replace(n, m, x))
sort(nil) → nil
sort(cons(n, x)) → cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x)))

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(cons(0, nil))
min(cons(s(x0), nil))
min(cons(x0, cons(x1, x2)))
if_min(true, cons(x0, cons(x1, x2)))
if_min(false, cons(x0, cons(x1, x2)))
replace(x0, x1, nil)
replace(x0, x1, cons(x2, x3))
if_replace(true, x0, x1, cons(x2, x3))
if_replace(false, x0, x1, cons(x2, x3))
sort(nil)
sort(cons(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted some edges using various graph approximations

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

MIN(cons(n, cons(m, x))) → LE(n, m)
SORT(cons(n, x)) → REPLACE(min(cons(n, x)), n, x)
REPLACE(n, m, cons(k, x)) → EQ(n, k)
SORT(cons(n, x)) → MIN(cons(n, x))
IF_MIN(true, cons(n, cons(m, x))) → MIN(cons(n, x))
MIN(cons(n, cons(m, x))) → IF_MIN(le(n, m), cons(n, cons(m, x)))
IF_REPLACE(false, n, m, cons(k, x)) → REPLACE(n, m, x)
REPLACE(n, m, cons(k, x)) → IF_REPLACE(eq(n, k), n, m, cons(k, x))
EQ(s(n), s(m)) → EQ(n, m)
LE(s(n), s(m)) → LE(n, m)
SORT(cons(n, x)) → SORT(replace(min(cons(n, x)), n, x))
IF_MIN(false, cons(n, cons(m, x))) → MIN(cons(m, x))

The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(m)) → false
eq(s(n), 0) → false
eq(s(n), s(m)) → eq(n, m)
le(0, m) → true
le(s(n), 0) → false
le(s(n), s(m)) → le(n, m)
min(cons(0, nil)) → 0
min(cons(s(n), nil)) → s(n)
min(cons(n, cons(m, x))) → if_min(le(n, m), cons(n, cons(m, x)))
if_min(true, cons(n, cons(m, x))) → min(cons(n, x))
if_min(false, cons(n, cons(m, x))) → min(cons(m, x))
replace(n, m, nil) → nil
replace(n, m, cons(k, x)) → if_replace(eq(n, k), n, m, cons(k, x))
if_replace(true, n, m, cons(k, x)) → cons(m, x)
if_replace(false, n, m, cons(k, x)) → cons(k, replace(n, m, x))
sort(nil) → nil
sort(cons(n, x)) → cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x)))

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(cons(0, nil))
min(cons(s(x0), nil))
min(cons(x0, cons(x1, x2)))
if_min(true, cons(x0, cons(x1, x2)))
if_min(false, cons(x0, cons(x1, x2)))
replace(x0, x1, nil)
replace(x0, x1, cons(x2, x3))
if_replace(true, x0, x1, cons(x2, x3))
if_replace(false, x0, x1, cons(x2, x3))
sort(nil)
sort(cons(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 5 SCCs with 4 less nodes.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                    ↳ QDPOrderProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

LE(s(n), s(m)) → LE(n, m)

The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(m)) → false
eq(s(n), 0) → false
eq(s(n), s(m)) → eq(n, m)
le(0, m) → true
le(s(n), 0) → false
le(s(n), s(m)) → le(n, m)
min(cons(0, nil)) → 0
min(cons(s(n), nil)) → s(n)
min(cons(n, cons(m, x))) → if_min(le(n, m), cons(n, cons(m, x)))
if_min(true, cons(n, cons(m, x))) → min(cons(n, x))
if_min(false, cons(n, cons(m, x))) → min(cons(m, x))
replace(n, m, nil) → nil
replace(n, m, cons(k, x)) → if_replace(eq(n, k), n, m, cons(k, x))
if_replace(true, n, m, cons(k, x)) → cons(m, x)
if_replace(false, n, m, cons(k, x)) → cons(k, replace(n, m, x))
sort(nil) → nil
sort(cons(n, x)) → cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x)))

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(cons(0, nil))
min(cons(s(x0), nil))
min(cons(x0, cons(x1, x2)))
if_min(true, cons(x0, cons(x1, x2)))
if_min(false, cons(x0, cons(x1, x2)))
replace(x0, x1, nil)
replace(x0, x1, cons(x2, x3))
if_replace(true, x0, x1, cons(x2, x3))
if_replace(false, x0, x1, cons(x2, x3))
sort(nil)
sort(cons(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

LE(s(n), s(m)) → LE(n, m)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
LE(x1, x2) = LE(x1)
s(x1) = s(x1)

Lexicographic path order with status [19].
Precedence:

s₁ > LE₁

Status:

LE₁: [1]
s₁: multiset

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ PisEmptyProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(m)) → false
eq(s(n), 0) → false
eq(s(n), s(m)) → eq(n, m)
le(0, m) → true
le(s(n), 0) → false
le(s(n), s(m)) → le(n, m)
min(cons(0, nil)) → 0
min(cons(s(n), nil)) → s(n)
min(cons(n, cons(m, x))) → if_min(le(n, m), cons(n, cons(m, x)))
if_min(true, cons(n, cons(m, x))) → min(cons(n, x))
if_min(false, cons(n, cons(m, x))) → min(cons(m, x))
replace(n, m, nil) → nil
replace(n, m, cons(k, x)) → if_replace(eq(n, k), n, m, cons(k, x))
if_replace(true, n, m, cons(k, x)) → cons(m, x)
if_replace(false, n, m, cons(k, x)) → cons(k, replace(n, m, x))
sort(nil) → nil
sort(cons(n, x)) → cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x)))

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(cons(0, nil))
min(cons(s(x0), nil))
min(cons(x0, cons(x1, x2)))
if_min(true, cons(x0, cons(x1, x2)))
if_min(false, cons(x0, cons(x1, x2)))
replace(x0, x1, nil)
replace(x0, x1, cons(x2, x3))
if_replace(true, x0, x1, cons(x2, x3))
if_replace(false, x0, x1, cons(x2, x3))
sort(nil)
sort(cons(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF_MIN(true, cons(n, cons(m, x))) → MIN(cons(n, x))
MIN(cons(n, cons(m, x))) → IF_MIN(le(n, m), cons(n, cons(m, x)))
IF_MIN(false, cons(n, cons(m, x))) → MIN(cons(m, x))

The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(m)) → false
eq(s(n), 0) → false
eq(s(n), s(m)) → eq(n, m)
le(0, m) → true
le(s(n), 0) → false
le(s(n), s(m)) → le(n, m)
min(cons(0, nil)) → 0
min(cons(s(n), nil)) → s(n)
min(cons(n, cons(m, x))) → if_min(le(n, m), cons(n, cons(m, x)))
if_min(true, cons(n, cons(m, x))) → min(cons(n, x))
if_min(false, cons(n, cons(m, x))) → min(cons(m, x))
replace(n, m, nil) → nil
replace(n, m, cons(k, x)) → if_replace(eq(n, k), n, m, cons(k, x))
if_replace(true, n, m, cons(k, x)) → cons(m, x)
if_replace(false, n, m, cons(k, x)) → cons(k, replace(n, m, x))
sort(nil) → nil
sort(cons(n, x)) → cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x)))

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(cons(0, nil))
min(cons(s(x0), nil))
min(cons(x0, cons(x1, x2)))
if_min(true, cons(x0, cons(x1, x2)))
if_min(false, cons(x0, cons(x1, x2)))
replace(x0, x1, nil)
replace(x0, x1, cons(x2, x3))
if_replace(true, x0, x1, cons(x2, x3))
if_replace(false, x0, x1, cons(x2, x3))
sort(nil)
sort(cons(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

IF_MIN(true, cons(n, cons(m, x))) → MIN(cons(n, x))
MIN(cons(n, cons(m, x))) → IF_MIN(le(n, m), cons(n, cons(m, x)))
IF_MIN(false, cons(n, cons(m, x))) → MIN(cons(m, x))

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
IF_MIN(x1, x2) = IF_MIN(x2)
true = true
cons(x1, x2) = cons(x1, x2)
MIN(x1) = MIN(x1)
le(x1, x2) = le
false = false
s(x1) = x1
0 = 0

Lexicographic path order with status [19].
Precedence:

true > MIN₁ > IF_MIN₁
le > IF_MIN₁
false > cons₂ > MIN₁ > IF_MIN₁
0 > IF_MIN₁

Status:

MIN₁: multiset
true: multiset
IF_MIN₁: multiset
false: multiset
le: []
0: multiset
cons₂: [1,2]

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ PisEmptyProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(m)) → false
eq(s(n), 0) → false
eq(s(n), s(m)) → eq(n, m)
le(0, m) → true
le(s(n), 0) → false
le(s(n), s(m)) → le(n, m)
min(cons(0, nil)) → 0
min(cons(s(n), nil)) → s(n)
min(cons(n, cons(m, x))) → if_min(le(n, m), cons(n, cons(m, x)))
if_min(true, cons(n, cons(m, x))) → min(cons(n, x))
if_min(false, cons(n, cons(m, x))) → min(cons(m, x))
replace(n, m, nil) → nil
replace(n, m, cons(k, x)) → if_replace(eq(n, k), n, m, cons(k, x))
if_replace(true, n, m, cons(k, x)) → cons(m, x)
if_replace(false, n, m, cons(k, x)) → cons(k, replace(n, m, x))
sort(nil) → nil
sort(cons(n, x)) → cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x)))

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(cons(0, nil))
min(cons(s(x0), nil))
min(cons(x0, cons(x1, x2)))
if_min(true, cons(x0, cons(x1, x2)))
if_min(false, cons(x0, cons(x1, x2)))
replace(x0, x1, nil)
replace(x0, x1, cons(x2, x3))
if_replace(true, x0, x1, cons(x2, x3))
if_replace(false, x0, x1, cons(x2, x3))
sort(nil)
sort(cons(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

EQ(s(n), s(m)) → EQ(n, m)

The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(m)) → false
eq(s(n), 0) → false
eq(s(n), s(m)) → eq(n, m)
le(0, m) → true
le(s(n), 0) → false
le(s(n), s(m)) → le(n, m)
min(cons(0, nil)) → 0
min(cons(s(n), nil)) → s(n)
min(cons(n, cons(m, x))) → if_min(le(n, m), cons(n, cons(m, x)))
if_min(true, cons(n, cons(m, x))) → min(cons(n, x))
if_min(false, cons(n, cons(m, x))) → min(cons(m, x))
replace(n, m, nil) → nil
replace(n, m, cons(k, x)) → if_replace(eq(n, k), n, m, cons(k, x))
if_replace(true, n, m, cons(k, x)) → cons(m, x)
if_replace(false, n, m, cons(k, x)) → cons(k, replace(n, m, x))
sort(nil) → nil
sort(cons(n, x)) → cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x)))

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(cons(0, nil))
min(cons(s(x0), nil))
min(cons(x0, cons(x1, x2)))
if_min(true, cons(x0, cons(x1, x2)))
if_min(false, cons(x0, cons(x1, x2)))
replace(x0, x1, nil)
replace(x0, x1, cons(x2, x3))
if_replace(true, x0, x1, cons(x2, x3))
if_replace(false, x0, x1, cons(x2, x3))
sort(nil)
sort(cons(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

EQ(s(n), s(m)) → EQ(n, m)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
EQ(x1, x2) = EQ(x1)
s(x1) = s(x1)

Lexicographic path order with status [19].
Precedence:

s₁ > EQ₁

Status:

EQ₁: [1]
s₁: multiset

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ PisEmptyProof

                  ↳ QDP

                  ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(m)) → false
eq(s(n), 0) → false
eq(s(n), s(m)) → eq(n, m)
le(0, m) → true
le(s(n), 0) → false
le(s(n), s(m)) → le(n, m)
min(cons(0, nil)) → 0
min(cons(s(n), nil)) → s(n)
min(cons(n, cons(m, x))) → if_min(le(n, m), cons(n, cons(m, x)))
if_min(true, cons(n, cons(m, x))) → min(cons(n, x))
if_min(false, cons(n, cons(m, x))) → min(cons(m, x))
replace(n, m, nil) → nil
replace(n, m, cons(k, x)) → if_replace(eq(n, k), n, m, cons(k, x))
if_replace(true, n, m, cons(k, x)) → cons(m, x)
if_replace(false, n, m, cons(k, x)) → cons(k, replace(n, m, x))
sort(nil) → nil
sort(cons(n, x)) → cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x)))

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(cons(0, nil))
min(cons(s(x0), nil))
min(cons(x0, cons(x1, x2)))
if_min(true, cons(x0, cons(x1, x2)))
if_min(false, cons(x0, cons(x1, x2)))
replace(x0, x1, nil)
replace(x0, x1, cons(x2, x3))
if_replace(true, x0, x1, cons(x2, x3))
if_replace(false, x0, x1, cons(x2, x3))
sort(nil)
sort(cons(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

REPLACE(n, m, cons(k, x)) → IF_REPLACE(eq(n, k), n, m, cons(k, x))
IF_REPLACE(false, n, m, cons(k, x)) → REPLACE(n, m, x)

The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(m)) → false
eq(s(n), 0) → false
eq(s(n), s(m)) → eq(n, m)
le(0, m) → true
le(s(n), 0) → false
le(s(n), s(m)) → le(n, m)
min(cons(0, nil)) → 0
min(cons(s(n), nil)) → s(n)
min(cons(n, cons(m, x))) → if_min(le(n, m), cons(n, cons(m, x)))
if_min(true, cons(n, cons(m, x))) → min(cons(n, x))
if_min(false, cons(n, cons(m, x))) → min(cons(m, x))
replace(n, m, nil) → nil
replace(n, m, cons(k, x)) → if_replace(eq(n, k), n, m, cons(k, x))
if_replace(true, n, m, cons(k, x)) → cons(m, x)
if_replace(false, n, m, cons(k, x)) → cons(k, replace(n, m, x))
sort(nil) → nil
sort(cons(n, x)) → cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x)))

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(cons(0, nil))
min(cons(s(x0), nil))
min(cons(x0, cons(x1, x2)))
if_min(true, cons(x0, cons(x1, x2)))
if_min(false, cons(x0, cons(x1, x2)))
replace(x0, x1, nil)
replace(x0, x1, cons(x2, x3))
if_replace(true, x0, x1, cons(x2, x3))
if_replace(false, x0, x1, cons(x2, x3))
sort(nil)
sort(cons(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

REPLACE(n, m, cons(k, x)) → IF_REPLACE(eq(n, k), n, m, cons(k, x))
IF_REPLACE(false, n, m, cons(k, x)) → REPLACE(n, m, x)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
REPLACE(x1, x2, x3) = REPLACE(x3)
cons(x1, x2) = cons(x2)
IF_REPLACE(x1, x2, x3, x4) = x4
eq(x1, x2) = eq
false = false
s(x1) = x1
0 = 0
true = true

Lexicographic path order with status [19].
Precedence:

cons₁ > REPLACE₁
eq > true > REPLACE₁
0 > false > REPLACE₁
0 > true > REPLACE₁

Status:

REPLACE₁: multiset
true: multiset
false: multiset
eq: []
0: multiset
cons₁: multiset

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ PisEmptyProof

                  ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(m)) → false
eq(s(n), 0) → false
eq(s(n), s(m)) → eq(n, m)
le(0, m) → true
le(s(n), 0) → false
le(s(n), s(m)) → le(n, m)
min(cons(0, nil)) → 0
min(cons(s(n), nil)) → s(n)
min(cons(n, cons(m, x))) → if_min(le(n, m), cons(n, cons(m, x)))
if_min(true, cons(n, cons(m, x))) → min(cons(n, x))
if_min(false, cons(n, cons(m, x))) → min(cons(m, x))
replace(n, m, nil) → nil
replace(n, m, cons(k, x)) → if_replace(eq(n, k), n, m, cons(k, x))
if_replace(true, n, m, cons(k, x)) → cons(m, x)
if_replace(false, n, m, cons(k, x)) → cons(k, replace(n, m, x))
sort(nil) → nil
sort(cons(n, x)) → cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x)))

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(cons(0, nil))
min(cons(s(x0), nil))
min(cons(x0, cons(x1, x2)))
if_min(true, cons(x0, cons(x1, x2)))
if_min(false, cons(x0, cons(x1, x2)))
replace(x0, x1, nil)
replace(x0, x1, cons(x2, x3))
if_replace(true, x0, x1, cons(x2, x3))
if_replace(false, x0, x1, cons(x2, x3))
sort(nil)
sort(cons(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

SORT(cons(n, x)) → SORT(replace(min(cons(n, x)), n, x))

The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(m)) → false
eq(s(n), 0) → false
eq(s(n), s(m)) → eq(n, m)
le(0, m) → true
le(s(n), 0) → false
le(s(n), s(m)) → le(n, m)
min(cons(0, nil)) → 0
min(cons(s(n), nil)) → s(n)
min(cons(n, cons(m, x))) → if_min(le(n, m), cons(n, cons(m, x)))
if_min(true, cons(n, cons(m, x))) → min(cons(n, x))
if_min(false, cons(n, cons(m, x))) → min(cons(m, x))
replace(n, m, nil) → nil
replace(n, m, cons(k, x)) → if_replace(eq(n, k), n, m, cons(k, x))
if_replace(true, n, m, cons(k, x)) → cons(m, x)
if_replace(false, n, m, cons(k, x)) → cons(k, replace(n, m, x))
sort(nil) → nil
sort(cons(n, x)) → cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x)))

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(cons(0, nil))
min(cons(s(x0), nil))
min(cons(x0, cons(x1, x2)))
if_min(true, cons(x0, cons(x1, x2)))
if_min(false, cons(x0, cons(x1, x2)))
replace(x0, x1, nil)
replace(x0, x1, cons(x2, x3))
if_replace(true, x0, x1, cons(x2, x3))
if_replace(false, x0, x1, cons(x2, x3))
sort(nil)
sort(cons(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

SORT(cons(n, x)) → SORT(replace(min(cons(n, x)), n, x))

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
SORT(x1) = SORT(x1)
cons(x1, x2) = cons(x2)
replace(x1, x2, x3) = x3
min(x1) = x1
if_min(x1, x2) = if_min(x1)
false = false
le(x1, x2) = x1
true = true
if_replace(x1, x2, x3, x4) = x4
eq(x1, x2) = eq
0 = 0
s(x1) = s
nil = nil

Lexicographic path order with status [19].
Precedence:

SORT₁ > cons₁ > eq > false > nil
SORT₁ > cons₁ > eq > true > nil
if_min₁ > cons₁ > eq > false > nil
if_min₁ > cons₁ > eq > true > nil
0 > false > nil
0 > true > nil
s > eq > false > nil
s > eq > true > nil

Status:

true: multiset
SORT₁: [1]
false: multiset
eq: []
0: multiset
s: multiset
cons₁: [1]
nil: multiset
if_min₁: multiset

The following usable rules [14] were oriented:

if_replace(false, n, m, cons(k, x)) → cons(k, replace(n, m, x))
if_replace(true, n, m, cons(k, x)) → cons(m, x)
replace(n, m, cons(k, x)) → if_replace(eq(n, k), n, m, cons(k, x))
replace(n, m, nil) → nil

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ PisEmptyProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(m)) → false
eq(s(n), 0) → false
eq(s(n), s(m)) → eq(n, m)
le(0, m) → true
le(s(n), 0) → false
le(s(n), s(m)) → le(n, m)
min(cons(0, nil)) → 0
min(cons(s(n), nil)) → s(n)
min(cons(n, cons(m, x))) → if_min(le(n, m), cons(n, cons(m, x)))
if_min(true, cons(n, cons(m, x))) → min(cons(n, x))
if_min(false, cons(n, cons(m, x))) → min(cons(m, x))
replace(n, m, nil) → nil
replace(n, m, cons(k, x)) → if_replace(eq(n, k), n, m, cons(k, x))
if_replace(true, n, m, cons(k, x)) → cons(m, x)
if_replace(false, n, m, cons(k, x)) → cons(k, replace(n, m, x))
sort(nil) → nil
sort(cons(n, x)) → cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x)))

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(cons(0, nil))
min(cons(s(x0), nil))
min(cons(x0, cons(x1, x2)))
if_min(true, cons(x0, cons(x1, x2)))
if_min(false, cons(x0, cons(x1, x2)))
replace(x0, x1, nil)
replace(x0, x1, cons(x2, x3))
if_replace(true, x0, x1, cons(x2, x3))
if_replace(false, x0, x1, cons(x2, x3))
sort(nil)
sort(cons(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.